package com.opNaga.bpmp;

import com.opNaga.bpmp.connectingObject.messageFlow.MessageFlow;
import com.opNaga.bpmp.connectingObject.messageFlow.MessageFlowSource;
import com.opNaga.bpmp.connectingObject.sequenceFlow.SequenceFlow;
import com.opNaga.bpmp.connectingObject.sequenceFlow.SequenceFlowTarget;
import com.opNaga.bpmp.flowObject.gateway.ANDGateway;
import com.opNaga.bpmp.flowObject.gateway.XORGateway;
import com.opNaga.bpmp.swimlane.Pool;

import java.io.BufferedWriter;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.util.Collection;
import java.util.HashSet;
import java.util.Iterator;
import java.util.TreeSet;

/**
 * User: Junyi BEI
 * Date: 05/02/2012
 * Time: 02:04
 */
public class BPMPTranslator {
  public static String main() {
    return "MODULE main\n";
  }

  public static String varBlock(BPMPElement... pools) {
    String block = "VAR\n";

    Collection<String> atomics = new TreeSet<String>();
    for(BPMPElement pool : pools) {
      Iterator<BPMPElement> elementIt = ((Pool) pool).iterateAtomicElements();
      while(elementIt.hasNext()) {
        atomics.add(elementIt.next().getName());
      }
    }
    for(String atomic : atomics) {
      block += atomic + ": boolean;\n";
    }
    return block;
  }
  
  public static String goals(BPMPElement... pools) {
    String gs = "";
    for(BPMPElement pool : pools) {
      String candidateGoal = "";
      Iterator<BPMPElement> endIt = ((Pool)pool).iterateEnds();
      while(endIt.hasNext()) {
        BPMPElement end = endIt.next();
        candidateGoal = or(candidateGoal,f(end.getName()));
      }
      gs = and(gs, candidateGoal);
    }
    return nl(gs);
  }

  public static String singleTask(BPMPElement... pools) {
    String se = comment("Single Task Restriction");
    Collection<String> atomics = new TreeSet<String>();
    for(BPMPElement pool : pools) {
      Iterator<BPMPElement> elementIt = ((Pool) pool).iterateAtomicElements();
      while(elementIt.hasNext()) {
        atomics.add(elementIt.next().getName());
      }
    }
    for(String atomic : atomics) {
      String negSet = "";
      for(String neg : atomics) {
        if(neg != atomic) {
          negSet = and(negSet, neg(neg));
        }
      }
      se = nl(and(se, g(implies(atomic, negSet))));
    }
    return nl(se);
  }

  public static String forwardTrack(BPMPElement... pools) {
    String ft = comment("Temporal Order(1/2): Forward Tracking");
    Collection<BPMPElement> atomics = new HashSet<BPMPElement>();
    for(BPMPElement pool : pools) {
      Iterator<BPMPElement> elementIt = ((Pool) pool).iterateAtomicElements();
      while(elementIt.hasNext()) {
        BPMPElement element = elementIt.next();
        atomics.add(element);
      }
    }
    for(BPMPElement atomic : atomics) {
      if(XORGateway.class.isAssignableFrom(atomic.getClass()) && ((XORGateway) atomic).outwardSequenceFlowSize() > 0) {
        Iterator<BPMPElement> osfIt = ((XORGateway) atomic).iterateOutwardSequenceFlows();
        Collection<String> targets = new TreeSet<String>();
        String xorGateway = "";
        while(osfIt.hasNext()) {
          BPMPElement osf = osfIt.next();
          targets.add(((SequenceFlow) osf).getTarget().getName());
        }
        for(String current : targets) {
          String andGNeg = "";
          for(String rest : targets) {
            if(rest != current) {
              andGNeg = and(andGNeg, g(neg(rest)));
            }
          }
          xorGateway = or(xorGateway, implies(current, andGNeg));
        }
        ft = nl(and(ft, g(xorGateway)));
      } else if(ANDGateway.class.isAssignableFrom(atomic.getClass()) && ((ANDGateway) atomic).outwardSequenceFlowSize
          () > 0) {
        Iterator<BPMPElement> osfIt = ((ANDGateway) atomic).iterateOutwardSequenceFlows();
        Collection<String> targets = new TreeSet<String>();
        String andGateway = "";
        while(osfIt.hasNext()) {
          BPMPElement osf = osfIt.next();
          targets.add(((SequenceFlow) osf).getTarget().getName());
        }
        for(String current : targets) {
          String andFut = "";
          for(String rest : targets) {
            if(rest != current) {
              andFut = and(andFut, f(rest));
            }
          }
          andGateway = and(andGateway, implies(current, andFut));
        }
        ft = nl(and(ft, g(andGateway)));
      }
      if(MessageFlowSource.class.isAssignableFrom(atomic.getClass()) && ((MessageFlowSource) atomic)
          .outwardMessageFlowSize() > 0) {
        Collection<String> targets = new TreeSet<String>();
        Iterator<BPMPElement> omfIt = ((MessageFlowSource) atomic).iterateOutwardMessageFlows();
        while(omfIt.hasNext()) {
          BPMPElement omf = omfIt.next();
          BPMPElement target = ((MessageFlow) omf).getTarget();
          targets.add(target.getName());
        }
        String andNeg = "";
        for(String succeeder : targets) {
          andNeg = and(andNeg, neg(succeeder));
        }
        String atomicName = atomic.getName();
        ft = nl(and(ft, g(or(o(atomicName), andNeg))));
      }
    }
    return nl(ft);
  }

  public static String backwardTrack(BPMPElement... pools) {
    String bt = comment("Temporal Order(2/2): Backward Tracking");
    Collection<BPMPElement> atomics = new HashSet<BPMPElement>();
    for(BPMPElement pool : pools) {
      Iterator<BPMPElement> elementIt = ((Pool) pool).iterateAtomicElements();
      while(elementIt.hasNext()) {
        BPMPElement element = elementIt.next();
        atomics.add(element);
      }
    }
    for(BPMPElement atomic : atomics) {
      if(XORGateway.class.isAssignableFrom(atomic.getClass()) && ((XORGateway) atomic).inwardSequenceFlowSize() > 0) {
        Iterator<BPMPElement> isfIt = ((XORGateway) atomic).iterateInwardSequenceFlows();
        Collection<String> sources = new TreeSet<String>();
        String xorGateway = "";
        while(isfIt.hasNext()) {
          BPMPElement osf = isfIt.next();
          sources.add(((SequenceFlow) osf).getSource().getName());
        }
        for(String current : sources) {
          String andNegO = "";
          for(String rest : sources) {
            if(rest != current) {
              andNegO = and(andNegO, neg(o(rest)));
            }
          }
          xorGateway = or(xorGateway, and(o(current), andNegO));
        }
        bt = nl(and(bt, g(or(xorGateway, neg(atomic.getName())))));
      } else if(ANDGateway.class.isAssignableFrom(atomic.getClass()) && ((ANDGateway) atomic).inwardSequenceFlowSize
          () > 0) {
        Iterator<BPMPElement> isfIt = ((ANDGateway) atomic).iterateInwardSequenceFlows();
        Collection<String> sources = new TreeSet<String>();
        String andGateway = "";
        while(isfIt.hasNext()) {
          BPMPElement isf = isfIt.next();
          sources.add(((SequenceFlow) isf).getSource().getName());
        }
        for(String current : sources) {
          andGateway = and(andGateway, o(current));
        }
        bt = nl(and(bt, g(or(andGateway, neg(atomic.getName())))));
      }
      if(SequenceFlowTarget.class.isAssignableFrom(atomic.getClass()) && ((SequenceFlowTarget) atomic)
          .inwardSequenceFlowSize() > 0) {
        Collection<String> sources = new TreeSet<String>();
        Iterator<BPMPElement> isfIt = ((SequenceFlowTarget) atomic).iterateInwardSequenceFlows();
        while(isfIt.hasNext()) {
          BPMPElement isf = isfIt.next();
          BPMPElement source = ((SequenceFlow) isf).getSource();
          sources.add(source.getName());
        }
        String orO = "";
        for(String preceder : sources) {
          orO = or(orO, o(preceder));
        }
        bt = nl(and(bt, g(or(orO, neg(atomic.getName())))));
      }
    }
    return bt;
  }

  public static String init(BPMPElement... pools) {
    String ret = "INIT\nTRUE\n";
    return ret;
  }

  public static String trans(BPMPElement... pools) {
    String ret = "TRANS\nTRUE\n";
    return ret;
  }

  public static String tltspec(BPMPElement... pools) {
    String ret = "LTLSPEC\n";
    String logic = neg(and(goals(pools),and(singleTask(pools), and(forwardTrack(pools), backwardTrack(pools)))));
    return ret + logic;
  }

  public static String encode(BPMPElement... pools) {
    String ret = main();
    ret += varBlock(pools);
    ret += init(pools);
    ret += trans(pools);
    ret += tltspec(pools);
    return ret;
  }

  public static File encode(String fileName, BPMPElement... pools) {
    File outputFile = new File(fileName);
    if(outputFile.getParentFile() == null) {
      String name = outputFile.getName();
      if(!name.endsWith(".smv")) {
        name += ".smv";
      }
      name = "./smv/" + name;
      outputFile = new File(name);
    }
    String ret = main();
    ret += varBlock(pools);
    ret += init(pools);
    ret += trans(pools);
    ret += tltspec(pools);
    try {
      FileWriter fStream = new FileWriter(outputFile);
      BufferedWriter out = new BufferedWriter(fStream);
      out.write(ret);
      out.close();
    } catch(IOException ioE) {
      return null;
    }
    return outputFile;
  }

  private static String neg(String current) {
    return "!" + bracket(current);
  }

  private static String g(String current) {
    current = bracket(current);
    if(current.equals("TRUE")) {
      return "TRUE";
    }
    if(current.equals("FALSE")) {
      return "FALSE";
    }
    return "G " + current;
  }

  private static String f(String current) {
    current = bracket(current);
    if(current.equals("TRUE")) {
      return "TRUE";
    }
    if(current.equals("FALSE")) {
      return "FALSE";
    }
    return "F " + current;
  }

  private static String o(String current) {
    current = bracket(current);
    if(current.equals("TRUE")) {
      return "TRUE";
    }
    if(current.equals("FALSE")) {
      return "FALSE";
    }
    return "O " + current;
  }

  private static String nl(String current) {
    current = bracket(current.trim());
    if(current.equals("TRUE")) {
      return "TRUE";
    }
    if(current.equals("FALSE")) {
      return "FALSE";
    }
    return current + "\n";
  }

  private static String comment(String comment) {
    if(comment == null || comment.isEmpty()) {
      return "\n";
    }
//    return "--" + comment + "\n";
    return "";
  }

  private static String implies(String a, String b) {
    return or(neg(bracket(a)), bracket(b));
  }

  private static String or(String current, String next) {
    next = bracket(next);
    if(current.equals("TRUE") || next.equals("TRUE")) {
      return "TRUE";
    }
    if(current.equals("FALSE") && next.equals("FALSE")) {
      return "FALSE";
    }
    if(current.equals("FALSE")) {
      return bracket(next);
    }
    if(next.equals("FALSE")) {
      return bracket(current);
    }
    if(!current.trim().isEmpty()) {
      current = bracket(current) + " | ";
    }
    current += next;
    return current;
  }

  private static String and(String current, String next) {
    next = bracket(next);
    if(current.equals("FALSE") || next.equals("FALSE")) {
      return "FALSE";
    }
    if(current.equals("TRUE") && next.equals("TRUE")) {
      return "TRUE";
    }
    if(current.equals("TRUE")) {
      return bracket(next);
    }
    if(next.equals("TRUE")) {
      return bracket(current);
    }
    if(!current.trim().isEmpty()) {
      current = bracket(current) + " & ";
    }
    current += next;
    return current;
  }

  private static String bracket(String input) {
    if(input == null || input.isEmpty()) {
      return "TRUE";
    }
    if(input.startsWith("--")) {
      int lineEnd = input.indexOf('\n');
      if(lineEnd > 0) {
        if(lineEnd + 1 < input.length()) {
          return input.substring(0, lineEnd + 1) + bracket(input.substring(lineEnd + 1));
        } else {
          return input;
        }
      }
    }
    int length = input.length();
    int openBracketNumber = 0;
    for(int i = 0; i < length; i++) {
      char current = input.charAt(i);
      if(current == '(') {
        openBracketNumber++;
      } else if(current == ')') {
        openBracketNumber--;
      } else if(openBracketNumber < 1 && (current == '|' || current == '&' || (current == '-' && (i + 1 < length &&
          input.charAt(i + 1) == '>' || i - 1 > 0 && input.charAt(i - 1) == '<')) || (current == 'G' && (i + 1 <
          length && input.charAt(i + 1) == ' ')) || (current == 'F' && (i + 1 < length && input.charAt(i + 1) == ' ')
      ) || (current == 'O' && (i + 1 < length && input.charAt(i + 1) == ' ')))) {
        return "(" + input + ")";
      }
    }
    return input;
  }
}
